Nuprl Definition : ecl-trans 0,22

ecl-trans(x)
== ecl_ind(x;k,test.ecl-base-tuple(k;test);a,b,A,B.combine-ecl-tuples(A;B;a,b,n. 0<n  a(n)
==  b(n a(0);a,ba  b);a,b,A,B.combine-ecl-tuples2(A;B;x,a,b,n. isl(x)
==  (0<n  if outl(x) a(n) else b(n) fi  n= a(0)  b(0));ha,hb,eha,ehb,a,ba  ehb
==  b  eha);a,b,A,B.combine-ecl-tuples2(A;B;x,a,b,n. isl(x)
==  if outl(x) a(n) else b(n) fi;ha,hb,eha,ehb,a,ba  hb  ehb
==  b  ha  eha);a,A.reset-ecl-tuple(A);a,m,A.add-ecl-act(A;m);a,m,A.ecl-add-throw(A;m);a,l,A.ecl-add-catch(A;l)) 
latex


Definitionsecl ind, ecl-base-tuple(k;test), combine-ecl-tuples(A;B;f;g), i<j, i=j, #$n, combine-ecl-tuples2(A;B;f;g), isl(x), if b t else f fi, outl(x), f(a), x.A(x), p  q, p  q, b, reset-ecl-tuple(A), add-ecl-act(A;m), ecl-add-throw(A;m), ecl-add-catch(A;l)
FDL editor aliasesecl-trans

origin